Nuprl Lemma : subtype-top
11,40
postcript
pdf
T
:Type. (
T
r Top)
True
latex
ProofTree
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
P
&
Q
,
P
Q
,
P
Q
,
True
,
t
T
,
Top
Lemmas
top
wf
,
true
wf
origin
T:Type. (T 
r Top) 
True
T:Type. (T r Top) True
x:A. B(x) Q Q Q
T